Nuprl Lemma : ma-single-sframe_wf
11,40
postcript
pdf
l
:IdLnk,
tg
:Id,
L
:(Knd List). only
L
sends on (
l
with
tg
)
MsgA
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
only
L
sends on (
l
with
tg
)
,
,
f
(
x
)?
z
,
Valtype(
da
;
k
)
,
t
.1
,
x
.
t
(
x
)
,
if
b
then
t
else
f
fi
,
x
dom(
f
)
,
deq-member(
eq
;
x
;
L
)
,
reduce(
f
;
k
;
as
)
,
ff
,
Y
,
x
(
s
)
Lemmas
mk-ma
wf
,
fpf-empty
wf
,
Id
wf
,
Knd
wf
,
rationals
wf
,
ma-state
wf
,
bool
wf
,
top
wf
,
IdLnk
wf
,
fpf-single
wf
,
finite-prob-space
wf
origin
l:IdLnk, tg:Id, L:(Knd List). only L sends on (l with tg) 
MsgA l:IdLnk, tg:Id, L:(Knd List). only L sends on (l with tg) MsgA x:A. B(x) T
x. t(x) dom(f)